/**
 * Copyright (c) 2010-2011 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.vstte12.problem3;

import com.googlecode.syper.anno.BoundsChecks;
import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;
import com.googlecode.syper.anno.NullChecks;

import edu.cmu.cs.crystal.annotations.PassingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * <b><a href="https://sites.google.com/site/vstte2012/compet">VSTTE 2012 
 * Verification Challenge</a> Problem 3: Ring Buffer</b>.
 * <p>
 * We want to implement a <i>queue</i> data structure using a ring buffer.
 * The buffer is implemented as a class with instance methods.
 * To create a buffer use the constructor, {@link #RingBuffer(int)}.
 * We use pre-conditions to prevent calls to {@link #head()} and {@link #pop()}
 * when the buffer is empty (calls to {@link #push(int)} when the buffer is full,
 * respectively).
 * <p>
 * Verification tasks:
 * <ol>
 * <li><i>Safety:</i> Verify that every array access is made within bounds.
 * Verified automatically due to {@link BoundsChecks} annotation throughout the class.
 * <li><i>Behavior:</i> Verify the correctness of your implementation w.r.t. the 
 * first-in first-out semantics of a queue.
 * The verified {@link #push(int)} and {@link #pop()} post-conditions encode
 * the first-in-first-out semantics of a queue.
 * <li><i>Harness:</i> {@link #test(int, int, int)} is verified successfully
 * </ol>
 * @author kevin
 * @since Nov 8, 2011
 */
@BoundsChecks // 1. checks that array accesses in bounds
@NullChecks   // checks absence of NPEs
@PassingTest
@UseAnalyses("SymbolicChecker")
public final class RingBuffer {

	@Excl private int[] data;
	private int size;
	private int first;
	private int len;
	
	//@ invariant data != null;
	//@ invariant data.length == size;
	//@ invariant 0 <= first & first < size;
	//@ invariant 0 <= len & len <= size;
	
	/**
	 * takes a positive integer {@code n} as argument and returns a new ring buffer 
	 * with size {@code n} and length 0 (no element).
	 * @param n
	 */
	//@ requires 0 < n;
	//@ ensures size == n;
	//@ ensures len == 0;
	//@ ensures first == 0; 
	public RingBuffer(int n) {
		data = new int[n];
		size = n;
		first = 0;
		len = 0;
	}
	
	/** empties this ring buffer */
	//@ ensures len == 0;
	@Excl(mod = "len") public void clear() {
		excl: len = 0;
	}
	
	/**
	 * Returns the first element in the queue.  Ring buffer must not be empty.
	 * @return the first element in the queue
	 */
	//@ requires 0 < len;
	//@ ensures \result == data[first];
	@Imm public int head() {
		imm: return data[first];
	}
	
	/**
	 * Adds a new element {@code x} at the end of the queue.
	 * Ring buffer must not be full.
	 * @param x new element
	 */
	//@ requires len < size;
	//@ ensures len == \old(len) + 1;
	//@ ensures (\forall int k; 0 <= k & k < size; 
	//@  	k == (\old(first) + \old(len)) % \old(size) ? data[k] == x : data[k] == \old(data[k]));
	@Excl(mod = "len") public void push(int x) {
		excl: {
			data[(first + len) % size] = x;
			++len;
		}
	}
	
	/**
	 * Pops off this ring buffer's head (first element in the queue), and returns it.
	 * The ring buffer must not be empty.
	 * @return the now-removed previous head
	 */
	//@ requires 0 < len;
	//@ ensures \result == data[\old(first)];
	//@ ensures len == \old(len) - 1;
	//@ ensures first == (\old(first) + 1) % size;
	//@ ensures (\forall int k; 0 <= k & k < size; data[k] == \old(data[k]));
	@Excl(mod = {"first", "len"}) public int pop() {
		excl: {
			int result = data[first];
			first = (first + 1) % size;
			--len;
			return result;
		}
	}
	
	/**
	 * 3. The following test harness should be verified 
	 * @param x
	 * @param y
	 * @param z
	 */
	public static void test(int x, int y, int z) {
		@Excl RingBuffer b = new RingBuffer(2);
		b.push(x);
		b.push(y);
		int h = b.pop();
		assert h == x;
		b.push(z);
		h = b.pop();
		assert h == y;
		h = b.pop();
		assert h == z;
	}
}
